#ifndef _PDTNODE_H_
#define _PDTNODE_H_

#include <string>
#include <sstream>
#include <vector>

#include "PDTNodeDefs.h"
#include "PDTException.h"
#include "PDTTraversalIFC.h"
#include "PDTAntlrProperties.h"
#include <z3.h>

#include <assert.h>

//#define LEFT 0
//#define RIGHT 1
//:% s/class \([^; {:]*\).*/\1_Em,
class PDTCodeGraph;
class PDTGraphVisitor;
class PDTZ3Visitor;
class PDTSMT2Visitor;
class PDTPreCondition;
class PDTPostCondition;
class PDTBehaviors;


class PDTNode {
protected:
	//PDTCodeGraph * codeGraph;
	NodeId id;
	Z3_ast Z3node;

	vector<PDTNode*> parents;
	vector<PDTNode*> children;
    PDTANTLRProperty props;

    unsigned int idx;

public:
	int cloneID;

    bool hasParents() {
        return !parents.empty();
    }

    unsigned int getLine(unsigned int index=0) {
        return props.getLine(index);
    }

    int getCharPosition(unsigned int index=0){
        return props.getCharPosition(index);
    }

    long long getStart(unsigned int index=0){
        return props.getStart(index);
    }

    long long getStop(unsigned int index=0){
        return props.getStop(index);
    }

    unsigned int setLine(unsigned int & aLine){
        return props.setLine(aLine);
    }

    int setCharPosition(int & aCharPosition){
        return props.setCharPosition(aCharPosition);
    }

    long long setStart(long long & aStart){
        return props.setStart(aStart);
    }

    long long setStop(long long & aStop){
        return props.setStop(aStop);
    }

    PDTANTLRProperty & getProperty() {
        return props;
    }


    unsigned int getChildrenCountEx() const {
	return children.size();
    }

    PDTNode & getChildEx(unsigned int i) {
	PDTNode * child = children[i];
	return *child;
    }

    virtual const char * getNodeString () {
	return PDTNodeTypeStringMap[getType()];
    }

    virtual Traversal::RetType traverseEx(Traversal & ) = 0;

    //the eval functions evaluates the value of a node based on its children.
    //It returns a boolean to check whether the program should stop or not.
    virtual bool eval(PDTCodeGraph &CG){return true;}

    //nValue is the node representing the value of another node in the graph
    //It is initialized to the necessary node type depending on the node it is attached to
    //PDTNumConstInt for integer nodes, PDTNumConstBool for bool nodes, and so on.
    PDTNode* nValue;

    virtual PDTNode* getNValue(){return nValue;}

    //The function clone simply copies the content of a node to a new node and returns it.
    virtual PDTNode* clone(PDTCodeGraph &CG){return NULL;}

	////////////////////////////////////////////
	////**** Used for cloneID increment ****////
	bool touched;
	virtual void incrementCloneID()
	{
		for (unsigned int i = 0; i<children.size(); i++)
		{
			if(children[i]->isVar())
			{
				if (!(children[i]->touched))
				{
					children[i]->cloneID++;
					children[i]->touched = true;
				}
			}
			else
				children[i]->incrementCloneID();
		}
	}
	virtual void untouch() //reinitialize
	{
		for (unsigned int i = 0; i<children.size(); i++)
		{
			if(children[i]->isVar())
			{
				children[i]->touched = false;
			}
			else
				children[i]->untouch();
		}
	}
	////************************************////
	////////////////////////////////////////////

	NodeId getId() const;

	virtual vector<PDTNode*> & getParents();
	virtual vector<PDTNode*> & getChildren();

	virtual void
	addParent(PDTNode* parent);
	virtual void
	addChild(PDTNode* child);

	virtual NodeTypeEnum getType()=0;

	PDTNode(PDTCodeGraph &CG);

	PDTNode() {
		// default constructor need for PDTType.h
	}

	char * makeIVName(const char * prefix);

	void
	traverse(PDTGraphVisitor &gv);

	virtual void incrementDepth() {
	}
	; // This is important only in PDTStatement derivatives, the rest are all recursion terminators.

	virtual void printType() {
		cout << "no";
	}

	virtual
	~PDTNode();

	virtual char *
	makeUniqueName(const char * prefix);

	virtual stringstream &
	toString(stringstream &) const = 0;

    virtual Z3_ast
    Z3value(PDTZ3Visitor &ZV){ return Z3visit(ZV);}

	virtual Z3_ast
	Z3visit(PDTZ3Visitor & ZV);
	virtual Z3_ast Z3NodeVisit(PDTZ3Visitor &) {
		return Z3node;
	}

    virtual bool
    SMT2visit(PDTSMT2Visitor & ){
      return true;
    }

	virtual bool isExp() {
		return false;
	}
	virtual bool isVar() {
		return false;
	}
	virtual bool isSetVar() {
		return false;
	}
	virtual bool isSequenceVar() {
		return false;
	}
	virtual bool isNum() {
		return false;
	}
	virtual bool isBool() {
		return false;
	}

	virtual bool isType() {
		return false;
	}
	virtual bool isSet() {
		return false;
	}
	virtual bool isPair() {
		return false;
	}
	virtual bool isRelation() {
		return false;
	}
	virtual bool isSequence() {
		return false;
	}

	virtual bool isNumVar() {
		return false;
	}
	virtual bool isNumConstInt() {
		return false;
	}
	virtual bool isNumConstDbl() {
		return false;
	}
	virtual bool isBoolVar() {
		return false;
	}
	virtual bool isBoolConst() {
		return false;
	}

	virtual bool isAdd() {
		return false;
	}
	virtual bool isSubt() {
		return false;
	}
	virtual bool isMult() {
		return false;
	}
	virtual bool isDiv() {
		return false;
	}
	virtual bool isMod() {
		return false;
	}

	virtual bool isNeg() {
		return false;
	}

	virtual bool isAssign() {
		return false;
	}

    virtual bool isPiAssign() {
        return false;
    }

	virtual bool isIfElse() {
		return false;
	}
	virtual bool isWhile() {
		return false;
	}

	virtual bool isAnd() {
		return false;
	}
	virtual bool isOr() {
		return false;
	}

	virtual bool isLessThan() {
		return false;
	}
	virtual bool isGreaterThan() {
		return false;
	}
	virtual bool isEqualNum() {
		return false;
	}

	virtual bool isEqualBool() {
		return false;
	}

	virtual bool isNot() {
		return false;
	}

	virtual bool isListOfStatements() {
		return false;
	}
	virtual bool isLessThanEqual() {
		return false;
	}
	virtual bool isGreaterThanEqual() {
		return false;
	}

	virtual bool isAssert() {
		return false;
	}

	virtual bool isCondition() {
		return false;
	}

	virtual bool isPreCondition() {
		return false;
	}

	virtual bool isPostCondition() {
		return false;
	}

	virtual bool isInvariant() {
		return false;
	}

	virtual bool isForall() {
		return false;
	}
	virtual bool isExist() {
		return false;
	}
	virtual bool isQuantifier() {
		return false;
	}

	virtual bool isIntersection() {
		return false;
	}
	virtual bool isUnion() {
		return false;
	}
	virtual bool isComplement() {
		return false;
	}

	virtual bool isUnary() {
		return false;
	}
	virtual bool isBinary() {
		return false;
	}
	virtual bool isSequenceAccessNum() {
		return false;
	}
	virtual bool isSequenceAccessBool() {
		return false;
	}
	virtual bool isStatement() {
		return false;
	}

	virtual bool isBehavior() const {
		return false;
	}

	virtual bool isBehaviors() const {
		return false;
	}

	virtual bool isUnaryNumExpr() {
		return false;
	}

	virtual bool isExpNum() {
		return false;
	}

	virtual bool isFunctionCall() {
		return false;
	}

	virtual bool isFunctionDec() {
		return false;
	}

	virtual bool isSequenceAssign() {
		return false;
	}

	virtual bool isConstSequence() {
		return false;
	}
    virtual bool isSpecTriple() const {return false;}

	//Find the node containing the precondition: simply Loops over all nodes and their children
    virtual PDTPreCondition* findPre(const string & spec);

	//Find the node containing the postcondition: simply Loops over all nodes and their children
	virtual PDTPostCondition* findPost(const string & spec);

	//Find the node containing the behaviors: simply Loops over all nodes and their children
	virtual PDTBehaviors* findBehaviors(const string & spec);
};
#endif
